r-Prime(u) == (u | 1 in r) & (v, w:|r|. u | v * w in r  (u | v in r  u | w in r)) 

latex

---

clarification:

r-Prime(u) == (u | 1r in r) & (v:|r|, w:|r|. u | v (*r) w in r  (u | v in r  u | w in r)) 

latex

Up	rings 1
Wellformedness Lemmas	rprime wf
Definitions	P & Q, A, 1, x:A. B(x), |r|, P  Q, x f y, *, P  Q, a | b in r